halo2

重要提示: 这个库正在积极开发中，不应该在生产软件中使用.

文档

最低支持的 Rust 版本

需要 Rust 1.51 或者更高.

最低支持的 rust 版本 可以在 未来更改, 但是这会带来小版本的改变

并行控制方案

halo2 当前为并行计算使用 rayon . 设置 线程数量数量时使用 RAYON_NUM_THREADS 环境变量

许可证

Copyright 2020-2021 The Electric Coin Company.

你可以在 Bootstrap 开源许可证 1.0 版下使用这个包， 或者您可以选择任意更高版本 . 看这个文件 COPYING 去了解更多详细信息, 看这个文件 LICENSE-BOSL 了解 Bootstrap 开源许可证 1.0 版条款.

BOSL的目的是允许对包进行商业改进，同时确保所有改进都是开源的 . 看 这 去了解 BOSL 为什么存在.

概念

首先，我们将描述零知识证明系统背后的概念; halo 2 所使用的算法(一种电路描述); 以及我们用来构建电路实现的抽象概念

Proof systems

证明系统 的目标是能够证明有趣的数学或密码学语句.

Typically, in a given protocol we will want to prove families of statements that differ in their public inputs. The prover will also need to show that they know some private inputs that make the statement hold.

通常，在给定的协议中，我们想要证明不同于它们的公共输入的语句族。 证明者需要展示他们知道一些隐私输入来使语句成立

To do this we write down a relation, $\mathcal{R}$, that specifies which combinations of public and private inputs are valid.

为了做到上面所说的, 我们描绘了一个关系式, $\mathcal{R}$, 这个关系式指定哪些公共输入和隐私输入组合是有效的。

The terminology above is intended to be aligned with the ZKProof Community Reference.

上面的术语和 ZKProof Community Reference 是一致的

To be precise, we should distinguish between the relation $\mathcal{R}$, and its implementation to be used in a proof system. We call the latter a circuit.

准确地说，我们应该区分关系式 $\mathcal{R}$ 和它在证明系统中使用的实现。我们称后者为电路。

The language that we use to express circuits for a particular proof system is called an arithmetization. Usually, an arithmetization will define circuits in terms of polynomial constraints on variables over a field.

我们用来表示特定证明系统的电路的语言叫做arithmetization。 通常，一个算法会在多项式约束条件下定义电路,多项式中的变量在一个域中 。

The process of expressing a particular relation as a circuit is also sometimes called "arithmetization", but we'll avoid that usage.

表达一个特定关系的过程叫做电路, 有时也叫作 "算法", 但是我们避免这种称呼.

To create a proof of a statement, the prover will need to know the private inputs, and also intermediate values, called advice values, that are used by the circuit.

为了去创建一个语句的proof, 证明者需要知道 private input, 还有电路使用的中间值，又称为通知值。

We assume that we can compute advice values efficiently from the private and public inputs. The particular advice values will depend on how we write the circuit, not only on the high-level statement.

我们假设我们能高效的通过公开输入和隐私输入计算通知值. 具体的通知值依赖于于我们如何编写电路，而不仅仅取决于高级语句。

The private inputs and advice values are collectively called a witness.

隐私输入和通知值共同叫做 witness

Some authors use "witness" as just a synonym for private inputs. But in our usage, a witness includes advice, i.e. it includes all values that the prover supplies to the circuit.

有些作者在写 隐私输入时使用witness, 但是在我们的使用中, witness还包括 通知值, 即它包括证明者提供给电路的所有值。

For example, suppose that we want to prove knowledge of a preimage $x$ of a hash function $H$ for a digest $y$:

举个例子

• The private input would be the preimage $x$.

• 隐私输入是 原像 $x$

• The public input would be the digest $y$.

• 公开输入是 $y$

• The relation would be $\{(x,y):H(x)=y\}$.

• 关系式为 $\{(x,y):H(x)=y\}$.

• For a particular public input $Y$, the statement would be: $\{(x):H(x)=Y\}$.

• 对于特定的公共输入 $Y$, 语句是$\{(x):H(x)=Y\}$.

• The advice would be all of the intermediate values in the circuit implementing the hash function. The witness would be $x$ and the advice.

• advice是实现哈希函数的电路中的所有中间值。witness是$x$和advice。

A Non-interactive Argument allows a prover to create a proof for a given statement and witness. The proof is data that can be used to convince a verifier that there exists a witness for which the statement holds. The security property that such proofs cannot falsely convince a verifier is called soundness.

非交互式argument允许prover给给定的语句和witness创建一个proof. 证明是一个可以使验证者确信存在witness 并使数据成立的数据. 这种证明不能错误地说服验证者的安全特性称为可靠性。

A Non-interactive Argument of Knowledge (NARK) further convinces the verifier that the prover knew a witness for which the statement holds. This security property is called knowledge soundness, and it implies soundness.

非交互式证明(NARK)进一步使验证者确信证明者知道使语句成立的witness. 这个安全属性称为知识可靠性，它暗示了可靠性。

In practice knowledge soundness is more useful for cryptographic protocols than soundness: if we are interested in whether Alice holds a secret key in some protocol, say, we need Alice to prove that she knows the key, not just that it exists.

在实践中，知识的可靠性对于密码协议比可靠性更有用 : 如果我们对Alice是否在某个协议中持有密钥感兴趣，我们需要Alice证明她知道密钥，而不仅仅是密钥存在。

Knowledge soundness is formalized by saying that an extractor, which can observe precisely how the proof is generated, must be able to compute the witness.

知识的可靠性是通过一个提取器来形式化的，它可以精确地观察证明是如何生成的，能够计算witness。

This property is subtle given that proofs can be malleable. That is, depending on the proof system it may be possible to take an existing proof (or set of proofs) and, without knowing the witness(es), modify it/them to produce a distinct proof of the same or a related statement. Higher-level protocols that use malleable proof systems need to take this into account.

这个性质是微妙的，因为证明是可塑的。 也就是说，根据证明系统，可以采用现有的证明(或者证明集) 在不知道witness的情况下，修改witness 生成一个明显相同的证明或者是一个有关的语句. 修改证人的陈述，以提供有关陈述的清晰证明。 使用可塑证明系统的高级协议需要考虑到这一点.

Even without malleability, proofs can also potentially be replayed. For instance, we would not want Alice in our example to be able to present a proof generated by someone else, and have that be taken as a demonstration that she knew the key.

即使没有可塑性, 证明也很可能回放, 举个例子, 我们不希望在我们的例子中Alice能够提交别人生成的证明，并将其作为她知道密钥的证明。

If a proof yields no information about the witness (other than that a witness exists and was known to the prover), then we say that the proof system is zero knowledge.

如果一个证明中没有关于witness的信息(除此之外, witness存在并且prover 知道witness), 这时我们说证明系统是 零知识的

If a proof system produces short proofs —i.e. of length polylogarithmic in the circuit size— then we say that it is succinct. A succinct NARK is called a SNARK (Succinct Non-Interactive Argument of Knowledge).

如果证明系统生成了简短的证明, 即 ? 那么我们说这时 简洁的 一个简介的NARK 叫做 snark(简洁的非交互式证明)

By this definition, a SNARK need not have verification time polylogarithmic in the circuit size. Some papers use the term efficient to describe a SNARK with that property, but we'll avoid that term since it's ambiguous for SNARKs that support amortized or recursive verification, which we'll get to later.

根据这个定义, 一个SNARK 不需要? 有些论文使用术语efficient来描述具有这种性质的SNARK， 但我们将避免使用这个术语，因为它对于支持平摊或递归验证的SNARKs来说是语义是模糊的，我们稍后会讲到

A zk-SNARK is a zero-knowledge SNARK.

zk-SNARK 叫做零知识证明

PLONKish 算法

halo2 使用的运算方法 来自于 PLONK, 或者更准确地说，它的扩展UltraPLONK支持自定义门和查找arguments. 我们称之为 PLONKish.

PLONKish电路是用矩形矩阵值定义的. 我们称呼矩阵的行，列，单元格 用常规的称呼。

PLONKish电路依赖配置

• 一个有限域$\mathbb{F}$，其中单元格的值(对于给定的statement和witness)将是$\mathbb{F}$的元素.

• The number of columns in the matrix, and a specification of each column as being fixed, advice, or instance. Fixed columns are fixed by the circuit; advice columns correspond to witness values; and instance columns are normally used for public inputs (technically, they can be used for any elements shared between the prover and verifier).

• 矩阵中列的数量, 以及每个列的参数是固定、通知还是实例. 固定列是固定在电路中的. 通知列和witness 值一致. 实例列通常用于公开输入( 确切来说, 它们可以用于prover和verifier之间共享的任何元素).

• A subset of the columns that can participate in equality constraints.

• 可以参与相等约束的列的子集。

• A polynomial degree bound.

• 多项式次数约束

• A sequence of polynomial constraints. These are multivariate polynomials over $\mathbb{F}$ that must evaluate to zero for each row. The variables in a polynomial constraint may refer to a cell in a given column of the current row, or a given column of another row relative to this one (with wrap-around, i.e. taken modulo $n$). The maximum degree of each polynomial is given by the polynomial degree bound.

• 一个多项式约束的序列. 这是在 $\mathbb{F}$ 上的每行必须为0的多元多项式. 多项式约束中的变量可以指当前行的给定列中的单元格,也可以指与这行(即取模n)相关的另一行的给定列 每个多项式的最高次由这个多项式次数给出.

• A sequence of lookup arguments defined over tuples of input expressions (which are multivariate polynomials as above) and table columns.

• 一个查找 arguments在输入表达式(多元多项式)的元组和表列上定义

A PLONKish circuit also defines:

PLONKish电路还定义:

• The number of rows $n$ in the matrix. $n$ must correspond to the size of a multiplicative subgroup of ${\mathbb{F}}^{\times }$; typically a power of two.

• 矩阵的行数为 $n$. $n$ 必须对应于 ${\mathbb{F}}^{\times }$ 的可乘子群的大小;通常是 2的幂次方.

• A sequence of equality constraints, which specify that two given cells must have equal values.

• 一个由相等约束组成的数组，数组中指定两个给定单元格必须具有相等的值

• The values of the fixed columns at each row.

• 每行中固定列的值

From a circuit description we can generate a proving key and a verification key, which are needed for the operations of proving and verification for that circuit.

从电路描述中我们可以生成 电路的证明和验证操作所需要的 一个 证明key 和 一个 验证key

Note that we specify the ordering of columns, polynomial constraints, lookup arguments, and equality constraints, even though these do not affect the meaning of the circuit. This makes it easier to define the generation of proving and verification keys as a deterministic process.

请注意，我们指定了列的顺序、多项式约束、查找参数和等式约束，即使这些并不影响电路的含义。 这使得将证明和验证密钥的生成定义为确定性过程变得更加容易。

Typically, a configuration will define polynomial constraints that are switched off and on by selectors defined in fixed columns. For example, a constraint $q_i\cdot p(...)=0$ can be switched off for a particular row $i$ by setting $q_i=0$. In this case we sometimes refer to a set of constraints controlled by a set of selector columns that are designed to be used together, as a gate. Typically there will be a standard gate that supports generic operations like field multiplication and division, and possibly also custom gates that support more specialized operations.

通常，配置将定义多项式约束，这些约束由定义在固定列中的选择器关闭和开启。 例如，约束 $q_i\cdot p(...)=0$ 可以通过在第i行设置$q_i=0$来关闭。 在这种情况下，我们有时引用一组由一组选择器列控制的约束，这些选择器列被设计为一起使用，就像一个gate。 通常会有一个标准门， 它支持像字段乘法和除法这样的通用操作，也可能有一个支持更专用操作的自定义门.

芯片

在先前的章节中, 提到了 一个低层次的电路描述. 在实现电路时, 我们通常会使用以可审核性、效率、模块化和可表达性为目标的高层次的api

在api中使用的一些术语和概念是类比于集成电路的设计和布局.关于集成电路, 通过组合特定功能的高效预编译的 芯片 更容易获得上述理想的特性.

举个例子, 我们可能有 实现特定密码学原语 的芯片, 比如说 哈希函数, 或者加密算法 或者像标量乘法或配对这样的算法.

在UPA中，仅仅有执行域乘法和加法的标准门电路就可以建立任意逻辑, 然而, 使用自定义门电路可以获得非常显著的效率增益.

使用我们的API, 我们定义了"知道" 如何使用特定的自定义门集合的芯片. 这创建了一个将高级电路的实现与直接使用自定义门的复杂性隔离开的抽象层.

尽管有时我们需要 "身兼两职", 既写高层次的电路, 也要写高层次电路所需要的芯片. 这样做的目的是使代码更易于理解、审计和维护/重用. 通过这种结构排除了一些潜在的实现的错误.

UPA中的门通过 相对引用 引用单元格，即给定列中的单元格，以及相对于设置门选择器的给定偏移量的行. 当偏移非0时, 我们称之为 偏移参考 (也就是说, 偏移引用是 相对引用的子集).

和 绝对引用 对比, 相对引用使用了相同的约束, 能指向任意单元格

偏移引用的动机是减少配置中列的数量,从而减少证明的大小. 如果没有偏移引用，则需要一个列来保存自定义门引用的每个值, 以及我们需要使用相同的约束从电路的其他单元复制值到该列中. 使用偏移引用, 我们不仅需要更少的列, 我们也不需要为所有这些列支持相同的约束，这可以提高效率.

在R1CS(对于一些读者来说,可能这个算法更熟悉, 如果不是,也不要担心), 电路包含了无语义重要顺序的海量的门. 另一方面, 因为偏移引用, UPA电路中的行顺序 是 重要的 我们做一些简单的假定和定义一些抽象概念来控制结构的复杂性: 目的就是这样, 在工具层, 我们做了大多数的电路构造, 我们不处理相对引用或者是明确的门布局.

我们把一个电路分到一个 范围 中, 每一个范围都包含着一个不相交的单元格子集, 相对引用只指向 一个区域内. 芯片实现的部分职责是确保进行偏移引用的门被放置在区域的正确位置。

给定区域集合和形状, 我们将使用一个单独的 平面规划器 来决定每个区域放置在哪里(即起始行在哪里)。 有一个实现了通用算法的默认 平面规划器, 在你需要时, 你可以写你自己的 平面规划器.

平面规划一般会在矩阵中留下空隙, 因为在给定的行中,电路门没有使用所有可用的列. 它们尽可能由不需要偏移引用的门填充，这允许它们被放置在任何行上。

芯片也定义了查找表. 如果同一个查找 argument 定义了多个表, 可以使用标记列指明 每行使用了哪一个表. 也可能对多个表(受多项式次数界的限制)进行联合查找.

芯片组合

为了将几个芯片的功能结合起来，我们将它们组合在一棵树上. 最高层次的芯片定义一组固定列、通知列和实例列，然后指定它们应该如何在较低级别芯片之间分布。

在最简单的情况下，每个低层次芯片将使用与其他芯片分离的列。然而，在芯片之间共享一列也是允许的。 优化advice列的数量尤其重要，因为这会影响证明的大小。

结果(可能在优化之后)是一个UPA配置。我们的电路实现将在芯片上参数化， 并且可以通过顶层次芯片使用支持的底层芯片的任何特性。

我们希望不那么专业的用户通常能够找到支持他们需要的操作的现有芯片， 或者只需要对现有芯片做微小的修改。专家级用户可以完全控制[] 电路优化 的种类.

Our hope is that less expert users will normally be able to find an existing chip that supports the operations they need, or only have to make minor modifications to an existing chip. Expert users will have full control to do the kind of circuit optimizations that ECC is famous for 🙂.

工具

当实现一个电路时，我们可以直接使用我们选择的芯片的特性。 通常, 我们会通过 工具 使用他们. 这种间接方式是很有用的，因为由于效率和UPA的限制，芯片接口通常依赖于底层的实现细节. 工具接口可以提供更加便捷和稳定的, 从无关细节抽象化的 api

举个例子, 想一个哈希函数, 比如说 SHA-256. 芯片的接口支持 SHA-256 可能是依赖于内部的哈希函数设计, 例如消息调度和压缩功能之间的分离功能. 一致的工具接口可以提供更加便捷和熟悉的 更新/完成 API, 也能够在不需要芯片支持的情况下处理hash函数的一部分, 比如说 填充 功能. 这类似于通常通过软件库而不是直接访问cpu上加密原语的加速 指令。

工具能在高层次上为电路程序提供一个模块化,可重用的抽象概念, 类似于在像 libsnark, bellman 这样的库中使用. 不但需要 抽象 函数, 同样也需要抽象 类型, 例如特定大小的椭圆曲线上的点或整数类型.

用户手册

你来这里可能是因为你想写电路?太好了!

本节将指导你通过halo创建电路的过程。

Developer tools

The halo2 crate includes several utilities to help you design and implement your circuits.

Mock prover

halo2::dev::MockProver is a tool for debugging circuits, as well as cheaply verifying their correctness in unit tests. The private and public inputs to the circuit are constructed as would normally be done to create a proof, but MockProver::run instead creates an object that will test every constraint in the circuit directly. It returns granular error messages that indicate which specific constraint (if any) is not satisfied.

Circuit visualizations

The dev-graph feature flag exposes several helper methods for creating graphical representations of circuits.

halo2::dev::circuit_layout renders the circuit layout as a grid:

• Columns are layed out from left to right as advice, instance, and fixed. The order of columns is otherwise without meaning.
  • Advice columns have a red background.
  • Instance columns have a white background.
  • Fixed columns have a blue background.
• Regions are shown as labelled green boxes (overlaying the background colour). A region may appear as multiple boxes if some of its columns happen to not be adjacent.
• Cells that have been assigned to by the circuit will be shaded in grey. If any cells are assigned to more than once (which is usually a mistake), they will be shaded darker than the surrounding cells.

halo2::dev::circuit_dot_graph builds a DOT graph string representing the given circuit, which can then be rendered witha variety of layout programs. The graph is built from calls to Layouter::namespace both within the circuit, and inside the gadgets and chips that it uses.

Cost estimator

The cost-model binary takes high-level parameters for a circuit design, and estimates the verification cost, as well as resulting proof size.

Usage: cargo run --example cost-model -- [OPTIONS] k

Positional arguments:
  k                       2^K bound on the number of rows.

Optional arguments:
  -h, --help              Print this message.
  -a, --advice R[,R..]    An advice column with the given rotations. May be repeated.
  -i, --instance R[,R..]  An instance column with the given rotations. May be repeated.
  -f, --fixed R[,R..]     A fixed column with the given rotations. May be repeated.
  -g, --gate-degree D     Maximum degree of the custom gates.
  -l, --lookup N,I,T      A lookup over N columns with max input degree I and max table degree T. May be repeated.
  -p, --permutation N     A permutation over N columns. May be repeated.

For example, to estimate the cost of a circuit with three advice columns and one fixed column (with various rotations), and a maximum gate degree of 4:

<span class="katex"><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.7777700000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">c</span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord mathnormal" style="margin-right:0.02778em;">or</span><span class="mord mathnormal">u</span><span class="mord mathnormal">n</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord">−</span><span class="mord mathnormal">e</span><span class="mord mathnormal">x</span><span class="mord mathnormal">am</span><span class="mord mathnormal" style="margin-right:0.01968em;">pl</span><span class="mord mathnormal">ecos</span><span class="mord mathnormal">t</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.77777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">m</span><span class="mord mathnormal">o</span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.66666em;vertical-align:-0.08333em;"></span><span class="mord">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.72777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.66666em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">a</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">−</span><span class="mord">1</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord">411</span><span class="mord mathnormal" style="margin-right:0.13889em;">F</span><span class="mord mathnormal">ini</span><span class="mord mathnormal">s</span><span class="mord mathnormal">h</span><span class="mord mathnormal">e</span><span class="mord mathnormal">dd</span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="mopen">[</span><span class="mord mathnormal">u</span><span class="mord mathnormal">n</span><span class="mord mathnormal">o</span><span class="mord mathnormal">pt</span><span class="mord mathnormal">imi</span><span class="mord mathnormal">ze</span><span class="mord mathnormal">d</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">+</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal">b</span><span class="mord mathnormal" style="margin-right:0.03588em;">ug</span><span class="mord mathnormal">in</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">o</span><span class="mclose">]</span><span class="mord mathnormal">t</span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord mathnormal">e</span><span class="mord mathnormal">t</span><span class="mopen">(</span><span class="mord mathnormal">s</span><span class="mclose">)</span><span class="mord mathnormal">in</span><span class="mord">0.03</span><span class="mord mathnormal">s</span><span class="mord mathnormal" style="margin-right:0.00773em;">R</span><span class="mord mathnormal">u</span><span class="mord mathnormal">nnin</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord">‘</span><span class="mord mathnormal">t</span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.02778em;">r</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord mathnormal">e</span><span class="mord mathnormal">t</span><span class="mord">/</span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal">b</span><span class="mord mathnormal" style="margin-right:0.03588em;">ug</span><span class="mord">/</span><span class="mord mathnormal">e</span><span class="mord mathnormal">x</span><span class="mord mathnormal">am</span><span class="mord mathnormal" style="margin-right:0.01968em;">pl</span><span class="mord mathnormal">es</span><span class="mord">/</span><span class="mord mathnormal">cos</span><span class="mord mathnormal">t</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.77777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">m</span><span class="mord mathnormal">o</span><span class="mord mathnormal">d</span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.72777em;vertical-align:-0.08333em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8388800000000001em;vertical-align:-0.19444em;"></span><span class="mord mathnormal">a</span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">−</span><span class="mord">1</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord">1</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord">0</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span><span class="mbin">−</span><span class="mspace" style="margin-right:0.2222222222222222em;"></span></span><span class="base"><span class="strut" style="height:1.036108em;vertical-align:-0.286108em;"></span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mord">411‘</span><span class="mord mathnormal" style="margin-right:0.07153em;">C</span><span class="mord mathnormal">i</span><span class="mord mathnormal">rc</span><span class="mord mathnormal">u</span><span class="mord mathnormal">i</span><span class="mord mathnormal">t</span><span class="mord"><span class="mord mathnormal" style="margin-right:0.03148em;">k</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">11</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">ma</span><span class="mord"><span class="mord mathnormal">x</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.33610799999999996em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">d</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mord mathnormal">e</span><span class="mord mathnormal" style="margin-right:0.03588em;">g</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">4</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">a</span><span class="mord mathnormal">d</span><span class="mord mathnormal" style="margin-right:0.03588em;">v</span><span class="mord mathnormal">i</span><span class="mord mathnormal">c</span><span class="mord"><span class="mord mathnormal">e</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.151392em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">c</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mord mathnormal">o</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mord mathnormal">u</span><span class="mord mathnormal">mn</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">3</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mord mathnormal">oo</span><span class="mord mathnormal" style="margin-right:0.03148em;">k</span><span class="mord mathnormal">u</span><span class="mord mathnormal">p</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">0</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">p</span><span class="mord mathnormal" style="margin-right:0.02778em;">er</span><span class="mord mathnormal">m</span><span class="mord mathnormal">u</span><span class="mord mathnormal">t</span><span class="mord mathnormal">a</span><span class="mord mathnormal">t</span><span class="mord mathnormal">i</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mopen">[</span><span class="mclose">]</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">co</span><span class="mord mathnormal" style="margin-right:0.01968em;">l</span><span class="mord mathnormal">u</span><span class="mord mathnormal">m</span><span class="mord"><span class="mord mathnormal">n</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.15139200000000003em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight" style="margin-right:0.03588em;">q</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.286108em;"><span></span></span></span></span></span></span><span class="mord mathnormal">u</span><span class="mord mathnormal" style="margin-right:0.02778em;">er</span><span class="mord mathnormal">i</span><span class="mord mathnormal">es</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">7</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">p</span><span class="mord mathnormal">o</span><span class="mord mathnormal">in</span><span class="mord"><span class="mord mathnormal">t</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.151392em;"><span style="top:-2.5500000000000003em;margin-left:0em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mathnormal mtight">s</span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.15em;"><span></span></span></span></span></span></span><span class="mord mathnormal">e</span><span class="mord mathnormal">t</span><span class="mord mathnormal">s</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord">3</span><span class="mpunct">,</span><span class="mspace" style="margin-right:0.16666666666666666em;"></span><span class="mord mathnormal">es</span><span class="mord mathnormal">t</span><span class="mord mathnormal">ima</span><span class="mord mathnormal">t</span><span class="mord mathnormal" style="margin-right:0.02778em;">or</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mord mathnormal" style="margin-right:0.05764em;">E</span><span class="mord mathnormal">s</span><span class="mord mathnormal">t</span><span class="mord mathnormal">ima</span><span class="mord mathnormal">t</span><span class="mord mathnormal" style="margin-right:0.02778em;">or</span><span class="mpunct">,</span></span><span class="mord mathnormal" style="margin-right:0.13889em;">P</span><span class="mord mathnormal">roo</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">s</span><span class="mord mathnormal">i</span><span class="mord mathnormal">ze</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:0.8888799999999999em;vertical-align:-0.19444em;"></span><span class="mord">1440</span><span class="mord mathnormal">b</span><span class="mord mathnormal" style="margin-right:0.03588em;">y</span><span class="mord mathnormal">t</span><span class="mord mathnormal">es</span><span class="mord mathnormal" style="margin-right:0.22222em;">V</span><span class="mord mathnormal" style="margin-right:0.02778em;">er</span><span class="mord mathnormal">i</span><span class="mord mathnormal" style="margin-right:0.10764em;">f</span><span class="mord mathnormal">i</span><span class="mord mathnormal">c</span><span class="mord mathnormal">a</span><span class="mord mathnormal">t</span><span class="mord mathnormal">i</span><span class="mord mathnormal">o</span><span class="mord mathnormal">n</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span><span class="mrel">:</span><span class="mspace" style="margin-right:0.2777777777777778em;"></span></span><span class="base"><span class="strut" style="height:0.69444em;vertical-align:0em;"></span><span class="mord mathnormal">a</span><span class="mord mathnormal" style="margin-right:0.01968em;">tl</span><span class="mord mathnormal">e</span><span class="mord mathnormal">a</span><span class="mord mathnormal">s</span><span class="mord mathnormal">t</span><span class="mord">81.689</span><span class="mord mathnormal">m</span><span class="mord mathnormal">s</span><span class="mord">‘‘‘</span></span></span></span>

A simple example

Let's start with a simple circuit, to introduce you to the common APIs and how they are used. The circuit will take a public input $c$, and will prove knowledge of two private inputs $a$ and $b$ such that

$$a^2\cdot b^2=c.$$

Define instructions

Firstly, we need to define the instructions that our circuit will rely on. Instructions are the boundary between high-level gadgets and the low-level circuit operations. Instructions may be as coarse or as granular as desired, but in practice you want to strike a balance between an instruction being large enough to effectively optimize its implementation, and small enough that it is meaningfully reusable.

For our circuit, we will use three instructions:

• Load a private number into the circuit.
• Multiply two numbers.
• Expose a number as a public input to the circuit.

We also need a type for a variable representing a number. Instruction interfaces provide associated types for their inputs and outputs, to allow the implementations to represent these in a way that makes the most sense for their optimization goals.

{{#include ../../../examples/simple-example.rs:instructions}}

Define a chip implementation

For our circuit, we will build a chip that provides the above numeric instructions for a finite field.

{{#include ../../../examples/simple-example.rs:chip}}

Every chip needs to implement the Chip trait. This defines the properties of the chip that a Layouter may rely on when synthesizing a circuit, as well as enabling any initial state that the chip requires to be loaded into the circuit.

{{#include ../../../examples/simple-example.rs:chip-impl}}

Configure the chip

The chip needs to be configured with the columns, permutations, and gates that will be required to implement all of the desired instructions.

{{#include ../../../examples/simple-example.rs:chip-config}}

Implement chip traits

{{#include ../../../examples/simple-example.rs:instructions-impl}}

Build the circuit

Now that we have the instructions we need, and a chip that implements them, we can finally build our circuit!

{{#include ../../../examples/simple-example.rs:circuit}}

Testing the circuit

halo2::dev::MockProver can be used to test that the circuit is working correctly. The private and public inputs to the circuit are constructed as we will do to create a proof, but by passing them to MockProver::run we get an object that can test every constraint in the circuit, and tell us exactly what is failing (if anything).

{{#include ../../../examples/simple-example.rs:test-circuit}}

Full example

You can find the source code for this example here.

Lookup tables

In normal programs, you can trade memory for CPU to improve performance, by pre-computing and storing lookup tables for some part of the computation. We can do the same thing in halo2 circuits!

A lookup table can be thought of as enforcing a relation between variables, where the relation is expressed as a table. Assuming we have only one lookup argument in our constraint system, the total size of tables is constrained by the size of the circuit: each table entry costs one row, and it also costs one row to do each lookup.

TODO

Gadgets

Tips and tricks

This section contains various ideas and snippets that you might find useful while writing halo2 circuits.

Small range constraints

A common constraint used in R1CS circuits is the boolean constraint: $b\ast (1-b)=0$. This constraint can only be satisfied by $b=0$ or $b=1$.

In halo2 circuits, you can similarly constrain a cell to have one of a small set of values. For example, to constrain $a$ to the range $[\mathrm{0..5}]$, you would create a gate of the form:

$$a\cdot (1-a)\cdot (2-a)\cdot (3-a)\cdot (4-a)=0$$

while to constraint $c$ to be either 7 or 13, you would use:

$$(7-c)\cdot (13-c)=0$$

The underlying principle here is that we create a polynomial constraint with roots at each value in the set of possible values we want to allow. In R1CS circuits, the maximum supported polynomial degree is 2 (due to all constraints being of the form $a\ast b=c$). In halo2 circuits, you can use arbitrary-degree polynomials - with the proviso that higher-degree constraints are more expensive to use.

Note that the roots don't have to be constants; for example $(a-x)\cdot (a-y)\cdot (a-z)=0$ will constrain $a$ to be equal to one of $\{x,y,z\}$ where the latter can be arbitrary polynomials, as long as the whole expression stays within the maximum degree bound.

Small set interpolation

We can use Lagrange interpolation to create a polynomial constraint that maps $f(X)=Y$ for small sets of $X\in \{x_i\},Y\in \{y_i\}$.

For instance, say we want to map a 2-bit value to a "spread" version interleaved with zeros. We first precompute the evaluations at each point:

$$\begin{array}{rcl}00\to 0000& ⟹& 0\to 0\\ 01\to 0001& ⟹& 1\to 1\\ 10\to 0100& ⟹& 2\to 4\\ 11\to 0101& ⟹& 3\to 5\end{array}$$

Then, we construct the Lagrange basis polynomial for each point using the identity: $$l_j(X)=\prod _{0\le m<k,m\ne j}\frac{x-x_m}{x_j-x_m},$$ where $k$ is the number of data points. ($k=4$ in our example above.)

Recall that the Lagrange basis polynomial $l_j(X)$ evaluates to $1$ at $X=x_j$ and $0$ at all other $x_i,j\ne i.$

Continuing our example, we get four Lagrange basis polynomials:

$$\begin{array}{ccc}{l}_0(X)& =& \frac{(X-3)(X-2)(X-1)}{(-3)(-2)(-1)}\\ l_1(X)& =& \frac{(X-3)(X-2)(X)}{(-2)(-1)(1)}\\ l_2(X)& =& \frac{(X-3)(X-1)(X)}{(-1)(1)(2)}\\ l_3(X)& =& \frac{(X-2)(X-1)(X)}{(1)(2)(3)}\end{array}$$

Our polynomial constraint is then

$$\begin{array}{cccccccccccl}& f(0)\cdot l_0(X)& +& f(1)\cdot l_1(X)& +& f(2)\cdot l_2(X)& +& f(3)\cdot l_3(X)& -& f(X)& =& 0\\ ⟹& 0\cdot l_0(X)& +& 1\cdot l_1(X)& +& 4\cdot l_2(X)& +& 5\cdot l_3(X)& -& f(X)& =& 0.\end{array}$$

Design

Note on Language

We use slightly different language than others to describe PLONK concepts. Here's the overview:

1. We like to think of PLONK-like arguments as tables, where each column corresponds to a "wire". We refer to entries in this table as "cells".
2. We like to call "selector polynomials" and so on "fixed columns" instead. We then refer specifically to a "selector constraint" when a cell in a fixed column is being used to control whether a particular constraint is enabled in that row.
3. We call the other polynomials "advice columns" usually, when they're populated by the prover.
4. We use the term "rule" to refer to a "gate" like $$A(X)\cdot q_A(X)+B(X)\cdot q_B(X)+A(X)\cdot B(X)\cdot q_M(X)+C(X)\cdot q_C(X)=0.$$
   • TODO: Check how consistent we are with this, and update the code and docs to match.

Proving system

The Halo 2 proving system can be broken down into five stages:

1. Commit to polynomials encoding the main components of the circuit:
   • Cell assignments.
   • Permuted values and products for each lookup argument.
   • Equality constraint permutations.
2. Construct the vanishing argument to constrain all circuit relations to zero:
   • Standard and custom gates.
   • Lookup argument rules.
   • Equality constraint permutation rules.
3. Evaluate the above polynomials at all necessary points:
   • All relative rotations used by custom gates across all columns.
   • Vanishing argument pieces.
4. Construct the multipoint opening argument to check that all evaluations are consistent with their respective commitments.
5. Run the inner product argument to create a polynomial commitment opening proof for the multipoint opening argument polynomial.

These stages are presented in turn across this section of the book.

Example

To aid our explanations, we will at times refer to the following example constraint system:

• Four advice columns $a,b,c,d$.
• One fixed column $f$.
• Three custom gates:
  • $a\cdot b\cdot c_{-1}-d=0$
  • $f_{-1}\cdot c=0$
  • $f\cdot d\cdot a=0$

tl;dr

The table below provides a (probably too) succinct description of the Halo 2 protocol. This description will likely be replaced by the Halo 2 paper and security proof, but for now serves as a summary of the following sub-sections.

Then the prover and verifier:

• Construct $\text{finalPoly}(X)$ as a linear combination of $\mathbf{Q}$ and $U$ using powers of $x_4$;
• Construct $\text{finalPolyEval}$ as the equivalent linear combination of ${\mathbf{q}}_{\text{evals}}$ and $u_{\text{eval}}$; and
• Perform $\text{InnerProduct}(\text{finalPoly}(X),x_3,\text{finalPolyEval}).$

TODO: Write up protocol components that provide zero-knowledge.

查找（Lookup）论据

halo2实现任意集合的数据查找，相比Plookup简单。

语言（Language）说明

除了 语言的一般说明:

• $Z(X)$多项式（针对置换论据的大乘积论据多项式）称为“置换乘积”列。

技术描述

为了解释简单，我们先描述一个忽略零知识证明的论据描述的简单版本。

查找可以表示成 $2^k$行表（编号从0开始）的“子集”。$A$和$S$列分别是“子集”和“全集”。

“子集”论据保证$A$列中的元素都在 $S$列中。这意味着，$A$列中多个位置的元素对应着$S$列中同一位置的元素，并且$S$列中的某些元素可以不出现在$A$列的任何位置上。

• $S$ 列并不一定是固定的。也就是说，我们可以支持固定元素的查找或者动态查找（后者采用advice列）。
• $A$ 和$S$列中的元素可以重复。如果$A$ 和$S$列中的元素个数不正好是$2^k$的话，可以用$A$ 和$S$列中任意元素进行扩展。
  • 或者我们可以增加一个“查找选择子”，控制在$A$列中的哪些元素参与查找。采用这种方法可以替换下述公式中的$A(X)$ 。如果一个元素不需要查找，用$S_0$替换$A$。

假设 ${\ell }_i$ 是拉格朗日基多项式，在$i$行多项式为1，其他行为0。

从$A$ 和$S$列的置换开始。假设它们的置换分别为$A^{\prime }$ 和 $S^{\prime }$列。我们可以通过置换论据$Z$约束它们之间的置换关系： $$Z(\omega X)\cdot (A^{\prime }(X)+\beta )\cdot (S^{\prime }(X)+\gamma )-Z(X)\cdot (A(X)+\beta )\cdot (S(X)+\gamma )=0$$$${\ell }_0(X)\cdot (1-Z(X))=0$$

也就是说，在除以0不发生的情况下，对所有的$i\in [0,2^k)$满足： $$Z_{i+1}=Z_i\cdot \frac{(A_i+\beta )\cdot (S_i+\gamma )}{(A_i^{\prime }+\beta )\cdot (S_i^{\prime }+\gamma )}$$$$Z_{2^k}=Z_0=1.$$

这个版本的论据证明$A^{\prime }$ 和 $S^{\prime }$列是$A$ 和$S$列的置换，但是并没有指明具体的置换关系。$\beta$ 和$\gamma$ 是独立因子。采用这两个因子，可以将两个置换论据组合在一起，不需要担心相互干扰。

这些置换的目的是让证明者提供的$A^{\prime }$ 和 $S^{\prime }$列满足一定的条件：

1. $A^{\prime }$列中相同的元素位置靠在一起。这可以通过某种排序算法实现。重要的是，相同的元素在$A^{\prime }$列中挨在一起，并且$A^{\prime }$列是$A$列的置换。
2. $A^{\prime }$列中挨在一起的相同元素的第一个元素存在于$S^{\prime }$列中。除去这个限制外，$S^{\prime }$列是$S$列的一个任意置换。

现在我们通过如下的规则限制$A_i^{\prime }=S_i^{\prime }$ 或者 $A_i^{\prime }=A_{i-1}^{\prime }$： $$(A^{\prime }(X)-S^{\prime }(X))\cdot (A^{\prime }(X)-A^{\prime }({\omega }^{-1}X))=0$$

除此之外，我们通过如下的规则限制$A_0^{\prime }=S_0^{\prime }$：

$${\ell }_0(X)\cdot (A^{\prime }(X)-S^{\prime }(X))=0$$

由于第二个规则，第一个规则中的($A^{\prime }(X)-A^{\prime }({\omega }^{-1}X)$ 这一项在$0$行没有效果，尽管 ${\omega }^{-1}X$ “能反转”。

这些约束规则一起有效的限制了$A^{\prime }$列（也就是$A$列）中的每个元素都存在于 $S^{\prime }$列中（也就是$S$列）。

加入零知识

为了在PLONK算法为基础的证明系统中加入零知识，我们需要在每列的最后加入$t$个随机元素。这些需要对查找论据进行调整，因为这些随机的元素并不满足之前的约束。

我们限制有效的行数为$u=2^k-t-1$。我们增加两个选择子：

• $q_{blind}$ 在最后 $t$ 行设置为1，其他行设置为0；
• $q_{last}$ 只在$u$行设置为1，其他行设置为0 （也就是说，它设置在有效行和盲化行的交界处）。

我们将之前的规则限制在有效行上：

$$(1-(q_{last}(X)+q_{blind}(X)))\cdot (Z(\omega X)\cdot (A^{\prime }(X)+\beta )\cdot (S^{\prime }(X)+\gamma )-Z(X)\cdot (A(X)+\beta )\cdot (S(X)+\gamma ))=0$$$$(1-(q_{last}(X)+q_{blind}(X)))\cdot (A^{\prime }(X)-S^{\prime }(X))\cdot (A^{\prime }(X)-A^{\prime }({\omega }^{-1}X))=0$$

在$0$行的限制规则保持不变：

$${\ell }_0(X)\cdot (A^{\prime }(X)-S^{\prime }(X))=0$$$${\ell }_0(X)\cdot (1-Z(X))=0$$

因为我们不能再依赖在 ${\omega }^{2^k}$点的环绕保证$Z$为1，相反我们要约束$Z({\omega }^u)$ 为1。这里有个难点：如果在任意$i\in [0,u)$， $A_i+\beta$ 或者 $S_i+\gamma$为0的话，置换论据可能不成立。虽然这种情况在 $\beta$ 和$\gamma$的取值下概率可以忽略，但是，对于完美零知识和完备性来说是个障碍（攻击者可以构造这样的情况）。

确保完美的完备性和零知识，我们允许$Z({\omega }^u)$为0或者1: $$q_{last}(X)\cdot (Z(X{)}^2-Z(X))=0$$

如果$A_i+\beta$ 和 $S_i+\gamma$在某些$i$ 上为0，我们可以在$i<j\le u$范围设置$Z_j=0$，满足上述的约束。

注意的是，挑战因子$\beta$ 和$\gamma$ 是在$A$ 和$S$列（以及$A^{\prime }$ 和 $S^{\prime }$列）承诺后生成的，证明者无法伪造$A_i+\beta$ 和 $S_i+\gamma$为0的情况。因为这种情况的概率可以忽略，可行性不受影响。

开销

• 原始$A$列和固定$S$列。
• 置换函数 $Z$。
• 两个置换$A^{\prime }$ 和 $S^{\prime }$列。
• 约束方程（门）的阶都不高。

泛化

halo2的查找论据实现实现了上述技术的泛化：

• $A$ 和$S$列扩展为多列，这些列之间通过随机挑战因子进行组合。$A^{\prime }$ 和 $S^{\prime }$列还是单列。
  • $S$列的各列承诺可以提前计算。这样在挑战因子确定后，利用Pedersen承诺的同态性质，可以很简便的组合。
  • $A$列可以是采用相对引用的任意多项式表达式。这些可以替换到约束规则中去，受制于最大的阶。这样可能可以省去一个或者多个advice列。
• 这样的话，任意关系的查找论据可以通过子集论据实现。也就是说，为了约束$\mathcal{R}(x,y,...)$，考虑$\mathcal{R}$是$S$的子集（通过前面的方法），并且检查关系成立 $(x,y,...)\in \mathcal{R}$。
  • 如果$\mathcal{R}$代表一个函数，同样需要检查输入是否在域中。这是我们想要的，经常会省去额外的范围检查。In the case where $\mathcal{R}$ represents a function, this implicitly also checks that the inputs are in the domain. This is typically what we want, and often saves an additional range check.
• 我们可以在同一个电路中支持多表。利用标示列将多个表组合成一张表。
  • 标示列可以和之前提到的“查找选择子”合并。

这些泛化和Plookup论文的第4和第5节中的技术类似。和Plookup的区别是子集论据。相关技术，子集论据也适用；举个例子，Plookup论文的第5节中的优化范围检查技术同样可以用在子集论据中。

Permutation argument

Given that gates in halo2 circuits operate "locally" (on cells in the current row or defined relative rows), it is common to need to copy a value from some arbitrary cell into the current row for use in a gate. This is performed with an equality constraint, which enforces that the source and destination cells contain the same value.

We implement these equality constraints by constructing a permutation that represents the constraints, and then using a permutation argument within the proof to enforce them.

Notation

A permutation is a one-to-one and onto mapping of a set onto itself. A permutation can be factored uniquely into a composition of cycles (up to ordering of cycles, and rotation of each cycle).

We sometimes use cycle notation to write permutations. Let $(abc)$ denote a cycle where $a$ maps to $b,$ $b$ maps to $c,$ and $c$ maps to $a$ (with the obvious generalization to arbitrary-sized cycles). Writing two or more cycles next to each other denotes a composition of the corresponding permutations. For example, $(ab)(cd)$ denotes the permutation that maps $a$ to $b,$ $b$ to $a,$ $c$ to $d,$ and $d$ to $c.$

Constructing the permutation

Goal

We want to construct a permutation in which each subset of variables that are in a equality-constraint set form a cycle. For example, suppose that we have a circuit that defines the following equality constraints:

• $a\equiv b$
• $a\equiv c$
• $d\equiv e$

From this we have the equality-constraint sets $\{a,b,c\}$ and $\{d,e\}.$ We want to construct the permutation:

$$(abc)(de)$$

which defines the mapping of $[a,b,c,d,e]$ to $[b,c,a,e,d].$

Algorithm

We need to keep track of the set of cycles, which is a set of disjoint sets. Efficient data structures for this problem are known; for the sake of simplicity we choose one that is not asymptotically optimal but is easy to implement.

We represent the current state as:

• an array $\mathsf{mapping}$ for the permutation itself;
• an auxiliary array $\mathsf{aux}$ that keeps track of a distinguished element of each cycle;
• another array $\mathsf{sizes}$ that keeps track of the size of each cycle.

We have the invariant that for each element $x$ in a given cycle $C,$ $\mathsf{aux}(x)$ points to the same element $c\in C.$ This allows us to quickly decide whether two given elements $x$ and $y$ are in the same cycle, by checking whether $\mathsf{aux}(x)=\mathsf{aux}(y).$ Also, $\mathsf{sizes}(\mathsf{aux}(x))$ gives the size of the cycle containing $x.$ (This is guaranteed only for $\mathsf{sizes}(\mathsf{aux}(x)),$ not for $\mathsf{sizes}(x).$)

The algorithm starts with a representation of the identity permutation: for all $x,$ we set $\mathsf{mapping}(x)=x,$ $\mathsf{aux}(x)=x,$ and $\mathsf{sizes}(x)=1.$

To add an equality constraint $left\equiv right$:

1. Check whether $left$ and $right$ are already in the same cycle, i.e. whether $\mathsf{aux}(left)=\mathsf{aux}(right).$ If so, there is nothing to do.
2. Otherwise, $left$ and $right$ belong to different cycles. Make $left$ the larger cycle and $right$ the smaller one, by swapping them iff $\mathsf{sizes}(\mathsf{aux}(left))<\mathsf{sizes}(\mathsf{aux}(right)).$
3. Set $\mathsf{sizes}(\mathsf{aux}(left)):=\mathsf{sizes}(\mathsf{aux}(left))+\mathsf{sizes}(\mathsf{aux}(right)).$
4. Following the mapping around the right (smaller) cycle, for each element $x$ set $\mathsf{aux}(x):=\mathsf{aux}(left).$
5. Splice the smaller cycle into the larger one by swapping $\mathsf{mapping}(left)$ with $\mathsf{mapping}(right).$

For example, given two disjoint cycles $(ABCD)$ and $(EFGH)$:

A +---> B
^       +
|       |
+       v
D <---+ C       E +---> F
                ^       +
                |       |
                +       v
                H <---+ G

After adding constraint $B\equiv E$ the above algorithm produces the cycle:

A +---> B +-------------+
^                       |
|                       |
+                       v
D <---+ C <---+ E       F
                ^       +
                |       |
                +       v
                H <---+ G

Broken alternatives

If we did not check whether $left$ and $right$ were already in the same cycle, then we could end up undoing an equality constraint. For example, if we have the following constraints:

• $a\equiv b$
• $b\equiv c$
• $c\equiv d$
• $b\equiv d$

and we tried to implement adding an equality constraint just using step 5 of the above algorithm, then we would end up constructing the cycle $(ab)(cd),$ rather than the correct $(abcd).$

Argument specification

We need to check a permutation of cells in $m$ columns, represented in Lagrange basis by polynomials $v_0,\dots ,v_{m-1}.$

We will label each cell in those $m$ columns with a unique element of ${\mathbb{F}}^{\times }.$

Suppose that we have a permutation on these labels, $$\sigma (\mathsf{column}:i,\mathsf{row}:j)=(\mathsf{column}:i^{\prime },\mathsf{row}:j^{\prime }).$$ in which the cycles correspond to equality-constraint sets.

If we consider the set of pairs $\{(label,value)\}$, then the values within each cycle are equal if and only if permuting the label in each pair by $\sigma$ yields the same set:

Since the labels are distinct, set equality is the same as multiset equality, which we can check using a product argument.

Let $\omega$ be a $2^k$ root of unity and let $\delta$ be a $T$ root of unity, where $T\cdot 2^S+1=p$ with $T$ odd and $k\le S.$ We will use ${\delta }^i\cdot {\omega }^j\in {\mathbb{F}}^{\times }$ as the label for the cell in the $j$th row of the $i$th column of the permutation argument.

We represent $\sigma$ by a vector of $m$ polynomials $s_i(X)$ such that $s_i({\omega }^j)={\delta }^{i^{\prime }}\cdot {\omega }^{j^{\prime }}.$

Notice that the identity permutation can be represented by the vector of $m$ polynomials ${\mathsf{ID}}_i({\omega }^j)$ such that ${\mathsf{ID}}_i({\omega }^j)={\delta }^i\cdot {\omega }^j.$

We will use a challenge $\beta$ to compress each $(label,value)$ pair to $value+\beta \cdot label.$ Just as in the product argument we used for lookups, we also use a challenge $\gamma$ to randomize each term of the product.

Now given our permutation represented by $s_0,\dots ,s_{m-1}$ over columns represented by $v_0,\dots ,v_{m-1},$ we want to ensure that: $$\prod _{i=0}^{m-1}\prod _{j=0}^{n-1}\left(\frac{v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }\right)=1$$

Here $v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j$ represents the unpermuted $(label,value)$ pair, and $v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)$ represents the permuted $(\sigma (label),value)$ pair.

Let $Z_P$ be such that $Z_P({\omega }^0)=Z_P({\omega }^n)=1$ and for $0\le j<n$: $$\begin{array}{rl}{Z}_P({\omega }^{j+1})& =\prod _{h=0}^j\prod _{i=0}^{m-1}\frac{v_i({\omega }^h)+\beta \cdot {\delta }^i\cdot {\omega }^h+\gamma }{v_i({\omega }^h)+\beta \cdot s_i({\omega }^h)+\gamma }\\ & =Z_P({\omega }^j)\prod _{i=0}^{m-1}\frac{v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }\end{array}$$

Then it is sufficient to enforce the rules: $$\begin{gathered} Z_P(\omega X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)=0 \\ {\ell }_0\cdot (1-Z_P(X))=0 \end{gathered}$$

This assumes that the number of columns $m$ is such that the polynomial in the first rule above fits within the degree bound of the PLONK configuration. We will see below how to handle a larger number of columns.

The optimization used to obtain the simple representation of the identity permutation was suggested by Vitalik Buterin for PLONK, and is described at the end of section 8 of the PLONK paper. Note that the ${\delta }^i$ are all distinct quadratic non-residues, provided that the number of columns that are enabled for equality is no more than $T$, which always holds in practice for the curves used in Halo 2.

Zero-knowledge adjustment

Similarly to the lookup argument, we need an adjustment to the above argument to account for the last $t$ rows of each column being filled with random values.

We limit the number of usable rows to $u=2^k-t-1.$ We add two selectors, defined in the same way as for the lookup argument:

• $q_{blind}$ is set to $1$ on the last $t$ rows, and $0$ elsewhere;
• $q_{last}$ is set to $1$ only on row $u,$ and $0$ elsewhere (i.e. it is set on the row in between the usable rows and the blinding rows).

We enable the product rule from above only for the usable rows:

$(1-(q_{last}(X)+q_{blind}(X)))\cdot$ $\left(Z_P(\omega X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=0}^{m-1}\left(v_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)\right)=0$

The rule that is enabled on row $0$ remains the same:

$${\ell }_0(X)\cdot (1-Z_P(X))=0$$

Since we can no longer rely on the wraparound to ensure that each product $Z_P$ becomes $1$ again at ${\omega }^{2^k},$ we would instead need to constrain $Z({\omega }^u)=1.$ This raises the same problem that was described for the lookup argument. So we allow $Z({\omega }^u)$ to be either zero or one:

$$q_{last}(X)\cdot (Z_P(X{)}^2-Z_P(X))=0$$

which gives perfect completeness and zero knowledge.

Spanning a large number of columns

The halo2 implementation does not in practice limit the number of columns for which equality constraints can be enabled. Therefore, it must solve the problem that the above approach might yield a product rule with a polynomial that exceeds the PLONK configuration's degree bound. The degree bound could be raised, but this would be inefficient if no other rules require a larger degree.

Instead, we split the product across $b$ sets of $m$ columns, using product columns $Z_{P,0},\dots Z_{P,b-1},$ and we use another rule to copy the product from the end of one column set to the beginning of the next.

That is, for $0\le a<b$ we have:

$(1-(q_{last}(X)+q_{blind}(X)))\cdot$ $\left(Z_{P,a}(\omega X)\cdot \prod _{i=am}^{(a+1)m-1}\left(v_i(X)+\beta \cdot s_i(X)+\gamma \right)-Z_P(X)\cdot \prod _{i=am}^{(a+1)m-1}\left(v_i(X)+\beta \cdot {\delta }^i\cdot X+\gamma \right)\right)$ $=0$

For simplicity this is written assuming that the number of columns enabled for equality constraints is a multiple of $m$; if not then the products for the last column set will have fewer than $m$ terms.

For the first column set we have:

$${\ell }_0\cdot (1-Z_{P,0}(X))=0$$

For each subsequent column set, $0<a<b,$ we use the following rule to copy $Z_{P,a-1}({\omega }^u)$ to the start of the next column set, $Z_{P,a}({\omega }^0)$:

$${\ell }_0\cdot \left(Z_{P,a}(X)-Z_{P,a-1}({\omega }^{u}X)\right)=0$$

For the last column set, we allow $Z_{P,b-1}({\omega }^u)$ to be either zero or one:

$$q_{last}(X)\cdot \left(Z_{P,b-1}(X{)}^2-Z_{P,b-1}(X)\right)=0$$

which gives perfect completeness and zero knowledge as before.

Circuit commitments

Committing to the circuit assignments

At the start of proof creation, the prover has a table of cell assignments that it claims satisfy the constraint system. The table has $n=2^k$ rows, and is broken into advice, instance, and fixed columns. We define $F_{i,j}$ as the assignment in the $j$th row of the $i$th fixed column. Without loss of generality, we'll similarly define $A_{i,j}$ to represent the advice and instance assignments.

We separate fixed columns here because they are provided by the verifier, whereas the advice and instance columns are provided by the prover. In practice, the commitments to instance and fixed columns are computed by both the prover and verifier, and only the advice commitments are stored in the proof.

To commit to these assignments, we construct Lagrange polynomials of degree $n-1$ for each column, over an evaluation domain of size $n$ (where $\omega$ is the $n$th primitive root of unity):

• $a_i(X)$ interpolates such that $a_i({\omega }^j)=A_{i,j}$.
• $f_i(X)$ interpolates such that $f_i({\omega }^j)=F_{i,j}$.

We then create a blinding commitment to the polynomial for each column:

$$\mathbf{A}=[\text{Commit}(a_0(X)),\dots ,\text{Commit}(a_i(X))]$$ $$\mathbf{F}=[\text{Commit}(f_0(X)),\dots ,\text{Commit}(f_i(X))]$$

$\mathbf{F}$ is constructed as part of key generation, using a blinding factor of $1$. $\mathbf{A}$ is constructed by the prover and sent to the verifier.

Committing to the lookup permutations

The verifier starts by sampling $\theta$, which is used to keep individual columns within lookups independent. Then, the prover commits to the permutations for each lookup as follows:

• Given a lookup with input column polynomials $[A_0(X),\dots ,A_{m-1}(X)]$ and table column polynomials $[S_0(X),\dots ,S_{m-1}(X)]$, the prover constructs two compressed polynomials

  $$A_{\text{compressed}}(X)={\theta }^{m-1}{A}_0(X)+{\theta }^{m-2}{A}_1(X)+\cdots +\theta A_{m-2}(X)+A_{m-1}(X)$$ $$S_{\text{compressed}}(X)={\theta }^{m-1}{S}_0(X)+{\theta }^{m-2}{S}_1(X)+\cdots +\theta S_{m-2}(X)+S_{m-1}(X)$$

• The prover then permutes $A_{\text{compressed}}(X)$ and $S_{\text{compressed}}(X)$ according to the rules of the lookup argument, obtaining $A^{\prime }(X)$ and $S^{\prime }(X)$.

The prover creates blinding commitments for all of the lookups

$$\mathbf{L}=\left[(\text{Commit}(A^{\prime }(X))),\text{Commit}(S^{\prime }(X))),\dots \right]$$

and sends them to the verifier.

After the verifier receives $\mathbf{A}$, $\mathbf{F}$, and $\mathbf{L}$, it samples challenges $\beta$ and $\gamma$ that will be used in the permutation argument and the remainder of the lookup argument below. (These challenges can be reused because the arguments are independent.)

Committing to the equality constraint permutation

Let $c$ be the number of columns that are enabled for equality constraints.

Let $m$ be the maximum number of columns that can accomodated by a column set without exceeding the PLONK configuration's polynomial degree bound.

Let $u$ be the number of “usable” rows as defined in the Permutation argument section.

Let $b=\mathsf{ceiling}(c/m).$

The prover constructs a vector $\mathbf{P}$ of length $bu$ such that for each column set $0\le a<b$ and each row $0\le j<u,$

$${\mathbf{P}}_{au+j}=\prod _{i=am}^{\min (c,(a+1)m)-1}\frac{v_i({\omega }^j)+\beta \cdot {\delta }^i\cdot {\omega }^j+\gamma }{v_i({\omega }^j)+\beta \cdot s_i({\omega }^j)+\gamma }.$$

The prover then computes a running product of $\mathbf{P}$, starting at $1$, and a vector of polynomials $Z_{P,\mathrm{0..}b-1}$ that each have a Lagrange basis representation corresponding to a $u$-sized slice of this running product, as described in the Permutation argument section.

The prover creates blinding commitments to each $Z_{P,a}$ polynomial:

$${\mathbf{Z}}_{\mathbf{P}}=\left[\text{Commit}(Z_{P,0}(X)),\dots ,\text{Commit}(Z_{P,b-1}(X))\right]$$

and sends them to the verifier.

Committing to the lookup permutation product columns

In addition to committing to the individual permuted lookups, for each lookup, the prover needs to commit to the permutation product column:

• The prover constructs a vector $P$:

$$P_j=\frac{(A_{\text{compressed}}({\omega }^j)+\beta )(S_{\text{compressed}}({\omega }^j)+\gamma )}{(A^{\prime }({\omega }^j)+\beta )(S^{\prime }({\omega }^j)+\gamma )}$$

• The prover constructs a polynomial $Z_L$ which has a Lagrange basis representation corresponding to a running product of $P$, starting at $Z_L(1)=1$.

$\beta$ and $\gamma$ are used to combine the permutation arguments for $A^{\prime }(X)$ and $S^{\prime }(X)$ while keeping them independent. The important thing here is that the verifier samples $\beta$ and $\gamma$ after the prover has created $\mathbf{A}$, $\mathbf{F}$, and $\mathbf{L}$ (and thus committed to all the cell values used in lookup columns, as well as $A^{\prime }(X)$ and $S^{\prime }(X)$ for each lookup).

As before, the prover creates blinding commitments to each $Z_L$ polynomial:

$${\mathbf{Z}}_{\mathbf{L}}=\left[\text{Commit}(Z_L(X)),\dots \right]$$

and sends them to the verifier.

Vanishing argument

Having committed to the circuit assignments, the prover now needs to demonstrate that the various circuit relations are satisfied:

• The custom gates, represented by polynomials ${\text{gate}}_i(X)$.
• The rules of the lookup arguments.
• The rules of the equality constraint permutations.

Each of these relations is represented as a polynomial of degree $d$ (the maximum degree of any of the relations) with respect to the circuit columns. Given that the degree of the assignment polynomials for each column is $n-1$, the relation polynomials have degree $d(n-1)$ with respect to $X$.

In our example, these would be the gate polynomials, of degree $3n-3$:

• ${\text{gate}}_0(X)=a_0(X)\cdot a_1(X)\cdot a_2(X{\omega }^{-1})-a_3(X)$
• ${\text{gate}}_1(X)=f_0(X{\omega }^{-1})\cdot a_2(X)$
• ${\text{gate}}_2(X)=f_0(X)\cdot a_3(X)\cdot a_0(X)$

A relation is satisfied if its polynomial is equal to zero. One way to demonstrate this is to divide each polynomial relation by the vanishing polynomial $t(X)=(X^n-1)$, which is the lowest-degree monomial that has roots at every ${\omega }^i$. If relation's polynomial is perfectly divisible by $t(X)$, it is equal to zero over the domain (as desired).

This simple construction would require a polynomial commitment per relation. Instead, we commit to all of the circuit relations simultaneously: the verifier samples $y$, and then the prover constructs the quotient polynomial

$$h(X)=\frac{{\text{gate}}_0(X)+y\cdot {\text{gate}}_1(X)+\cdots +y^i\cdot {\text{gate}}_i(X)+\dots }{t(X)},$$

where the numerator is a random (the prover commits to the cell assignments before the verifier samples $y$) linear combination of the circuit relations.

• If the numerator polynomial (in formal indeterminate $X$) is perfectly divisible by $t(X)$, then with high probability all relations are satisfied.
• Conversely, if at least one relation is not satisfied, then with high probability $h(x)\cdot t(x)$ will not equal the evaluation of the numerator at $x$. In this case, the numerator polynomial would not be perfectly divisible by $t(X)$.

Committing to $h(X)$

$h(X)$ has degree $(d-1)n-d$ (because the divisor $t(X)$ has degree $n$). However, the polynomial commitment scheme we use for Halo 2 only supports committing to polynomials of degree $n-1$ (which is the maximum degree that the rest of the protocol needs to commit to). Instead of increasing the cost of the polynomial commitment scheme, the prover split $h(X)$ into pieces of degree $n-1$

$$h_0(X)+X^n{h}_1(X)+\cdots +X^{n(d-1)}{h}_{d-1}(X),$$

and produces blinding commitments to each piece

$$\mathbf{H}=[\text{Commit}(h_0(X)),\text{Commit}(h_1(X)),\dots ,\text{Commit}(h_{d-1}(X))].$$

Evaluating the polynomials

At this point, all properties of the circuit have been committed to. The verifier now wants to see if the prover committed to the correct $h(X)$ polynomial. The verifier samples $x$, and the prover produces the purported evaluations of the various polynomials at $x$, for all the relative offsets used in the circuit, as well as $h(X)$.

In our example, this would be:

• $a_0(x)$
• $a_1(x)$
• $a_2(x)$, $a_2(x{\omega }^{-1})$
• $a_3(x)$
• $f_0(x)$, $f_0(x{\omega }^{-1})$
• $h_0(x)$, ..., $h_{d-1}(x)$

The verifier checks that these evaluations satisfy the form of $h(X)$:

$$\frac{{\text{gate}}_0(x)+\cdots +y^i\cdot {\text{gate}}_i(x)+\dots }{t(x)}=h_0(x)+\cdots +x^{n(d-1)}{h}_{d-1}(x)$$

Now content that the evaluations collectively satisfy the gate constraints, the verifier needs to check that the evaluations themselves are consistent with the original circuit commitments, as well as $\mathbf{H}$. To implement this efficiently, we use a multipoint opening argument.

Multipoint opening argument

Consider the commitments $A,B,C,D$ to polynomials $a(X),b(X),c(X),d(X)$. Let's say that $a$ and $b$ were queried at the point $x$, while $c$ and $d$ were queried at both points $x$ and $\omega x$. (Here, $\omega$ is the primitive root of unity in the multiplicative subgroup over which we constructed the polynomials).

To open these commitments, we could create a polynomial $Q$ for each point that we queried at (corresponding to each relative rotation used in the circuit). But this would not be efficient in the circuit; for example, $c(X)$ would appear in multiple polynomials.

Instead, we can group the commitments by the sets of points at which they were queried: $$\begin{array}{ccccc}& \{x\}& & \{x,\omega x\}& \\ & A& & C& \\ & B& & D& \end{array}$$

For each of these groups, we combine them into a polynomial set, and create a single $Q$ for that set, which we open at each rotation.

Optimization steps

The multipoint opening optimization takes as input:

• A random $x$ sampled by the verifier, at which we evaluate $a(X),b(X),c(X),d(X)$.
• Evaluations of each polynomial at each point of interest, provided by the prover: $a(x),b(x),c(x),d(x),c(\omega x),d(\omega x)$

These are the outputs of the vanishing argument.

The multipoint opening optimization proceeds as such:

1. Sample random $x_1$, to keep $a,b,c,d$ linearly independent.

2. Accumulate polynomials and their corresponding evaluations according to the point set at which they were queried: q_polys: $$\begin{array}{rcclc}{q}_1(X)& =& a(X)& +& x_{1}b(X)\\ q_2(X)& =& c(X)& +& x_{1}d(X)\end{array}$$ q_eval_sets:

           [
               [a(x) + x_1 b(x)],
               [
                   c(x) + x_1 d(x),
                   c(\omega x) + x_1 d(\omega x)
               ]
           ]
   

   NB: q_eval_sets is a vector of sets of evaluations, where the outer vector goes over the point sets, and the inner vector goes over the points in each set.

3. Interpolate each set of values in q_eval_sets: r_polys: $$\begin{array}{cccc}{r}_1(X)s.t.& & & \\ & r_1(x)& =& a(x)+x_{1}b(x)\\ r_2(X)s.t.& & & \\ & r_2(x)& =& c(x)+x_{1}d(x)\\ & r_2(\omega x)& =& c(\omega x)+x_{1}d(\omega x)\end{array}$$

4. Construct f_polys which check the correctness of q_polys: f_polys $$\begin{array}{rcl}{f}_1(X)& =& \frac{q_1(X)-r_1(X)}{X-x}\\ f_2(X)& =& \frac{q_2(X)-r_2(X)}{(X-x)(X-\omega x)}\end{array}$$

   If $q_1(x)=r_1(x)$, then $f_1(X)$ should be a polynomial. If $q_2(x)=r_2(x)$ and $q_2(\omega x)=r_2(\omega x)$ then $f_2(X)$ should be a polynomial.

5. Sample random $x_2$ to keep the f_polys linearly independent.

6. Construct $f(X)=f_1(X)+x_2{f}_2(X)$.

7. Sample random $x_3$, at which we evaluate $f(X)$: $$\begin{array}{rcccl}f(x_3)& =& f_1(x_3)& +& x_2{f}_2(x_3)\\ & =& \frac{q_1(x_3)-r_1(x_3)}{x_3-x}& +& x_2\frac{q_2(x_3)-r_2(x_3)}{(x_3-x)(x_3-\omega x)}\end{array}$$

8. Sample random $x_4$ to keep $f(X)$ and q_polys linearly independent.

9. Construct final_poly, $$final\_poly(X)=f(X)+x_4{q}_1(X)+x_4^2{q}_2(X),$$ which is the polynomial we commit to in the inner product argument.

Inner product argument

Halo 2 uses a polynomial commitment scheme for which we can create polynomial commitment opening proofs, based around the Inner Product Argument.

TODO: Explain Halo 2's variant of the IPA.

It is very similar to ${\text{PC}}_{\text{DL}}.\text{Open}$ from Appendix A.2 of BCMS20. See this comparison for details.

Comparison to other work

BCMS20 Appendix A.2

Appendix A.2 of BCMS20 describes a polynomial commitment scheme that is similar to the one described in BGH19 (BCMS20 being a generalization of the original Halo paper). Halo 2 builds on both of these works, and thus itself uses a polynomial commitment scheme that is very similar to the one in BCMS20.

The following table provides a mapping between the variable names in BCMS20, and the equivalent objects in Halo 2 (which builds on the nomenclature from the Halo paper):

Halo 2's polynomial commitment scheme differs from Appendix A.2 of BCMS20 in two ways:

1. Step 8 of the $\text{Open}$ algorithm computes a "non-hiding" commitment $C^{\prime }$ prior to the inner product argument, which opens to the same value as $C$ but is a commitment to a randomly-drawn polynomial. The remainder of the protocol involves no blinding. By contrast, in Halo 2 we blind every single commitment that we make (even for instance and fixed polynomials, though using a blinding factor of 1 for the fixed polynomials); this makes the protocol simpler to reason about. As a consequence of this, the verifier needs to handle the cumulative blinding factor at the end of the protocol, and so there is no need to derive an equivalent to $C^{\prime }$ at the start of the protocol.

   • $C^{\prime }$ is also an input to the random oracle for ${\xi }_0$; in Halo 2 we utilize a transcript that has already committed to the equivalent components of $C^{\prime }$ prior to sampling $z$.

2. The ${\text{PC}}_{\text{DL}}.\text{SuccinctCheck}$ subroutine (Figure 2 of BCMS20) computes the initial group element $C_0$ by adding $[v]H^{\prime }=[vϵ]H$, which requires two scalar multiplications. Instead, we subtract $[v]G_0$ from the original commitment $P$, so that we're effectively opening the polynomial at the point to the value zero. The computation $[v]G_0$ is more efficient in the context of recursion because $G_0$ is a fixed base (so we can use lookup tables).

Protocol Description

Preliminaries

We take $\lambda$ as our security parameter, and unless explicitly noted all algorithms and adversaries are probabilistic (interactive) Turing machines that run in polynomial time in this security parameter. We use $\text{negl}(\lambda )$ to denote a function that is negligible in $\lambda$.

Cryptographic Groups

We let $\mathbb{G}$ denote a cyclic group of prime order $p$. The identity of a group is written as $\mathcal{O}$. We refer to the scalars of elements in $\mathbb{G}$ as elements in a scalar field $\mathbb{F}$ of size $p$. Group elements are written in capital letters while scalars are written in lowercase or Greek letters. Vectors of scalars or group elements are written in boldface, i.e. $\mathbf{a}\in {\mathbb{F}}^n$ and $\mathbf{G}\in {\mathbb{G}}^n$. Group operations are written additively and the multiplication of a group element $G$ by a scalar $a$ is written $[a]G$.

We will often use the notation $⟨\mathbf{a},\mathbf{b}⟩$ to describe the inner product of two like-length vectors of scalars $\mathbf{a},\mathbf{b}\in {\mathbb{F}}^n$. We also use this notation to represent the linear combination of group elements such as $⟨\mathbf{a},\mathbf{G}⟩$ with $\mathbf{a}\in {\mathbb{F}}^n,\mathbf{G}\in {\mathbb{G}}^n$, computed in practice by a multiscalar multiplication.

We use $0^n$ to describe a vector of length $n$ that contains only zeroes in $\mathbb{F}$.

Discrete Log Relation Problem. The advantage metric $${\mathsf{Adv}}_{\mathbb{G},n}^{\mathsf{dl}-\mathsf{rel}}(\mathcal{A},\lambda )=\text{Pr}\left[{\mathsf{G}}_{\mathbb{G},n}^{\mathsf{dl}-\mathsf{rel}}(\mathcal{A},\lambda )\right]$$ is defined with respect the following game. $$\begin{array}{ll}& \underline{\mathbf{Game}{\mathsf{G}}_{\mathbb{G},n}^{\mathsf{dl}-\mathsf{rel}}(\mathcal{A},\lambda ):}\\ & \mathbf{G}\leftarrow {\mathbb{G}}_{\lambda }^n\\ & \mathbf{a}\leftarrow \mathcal{A}(\mathbf{G})\\ & \text{Return}\left(⟨\mathbf{a},\mathbf{G}⟩=\mathcal{O}\wedge \mathbf{a}\ne 0^n\right)\end{array}$$

Given an $n$-length vector $\mathbf{G}\in {\mathbb{G}}^n$ of group elements, the discrete log relation problem asks for $\mathbf{g}\in {\mathbb{F}}^n$ such that $\mathbf{g}\ne 0^n$ and yet $⟨\mathbf{g},\mathbf{G}⟩=\mathcal{O}$, which we refer to as a non-trivial discrete log relation. The hardness of this problem is tightly implied by the hardness of the discrete log problem in the group as shown in Lemma 3 of [JT20]. Formally, we use the game ${\mathsf{G}}_{\mathbb{G},n}^{\mathsf{dl}-\mathsf{rel}}$ defined above to capture this problem.

Interactive Proofs

Interactive proofs are a triple of algorithms $\text{IP}=(\text{Setup},\mathcal{P},\mathcal{V})$. The algorithm $\text{Setup}(1^{\lambda })$ produces as its output some public parameters commonly refered to by $\mathsf{pp}$. The prover $\mathcal{P}$ and verifier $\mathcal{V}$ are interactive machines (with access to $\mathsf{pp}$) and we denote by $⟨\mathcal{P}(x),\mathcal{V}(y)⟩$ an algorithm that executes a two-party protocol between them on inputs $x,y$. The output of this protocol, a transcript of their interaction, contains all of the messages sent between $\mathcal{P}$ and $\mathcal{V}$. At the end of the protocol, the verifier outputs a decision bit.

Zero knowledge Arguments of Knowledge

Proofs of knowledge are interactive proofs where the prover aims to convince the verifier that they know a witness $w$ such that $(x,w)\in \mathcal{R}$ for a statement $x$ and polynomial-time decidable relation $\mathcal{R}$. We will work with arguments of knowledge which assume computationally-bounded provers.

We will analyze arguments of knowledge through the lens of four security notions.

• Completeness: If the prover possesses a valid witness, can they always convince the verifier? It is useful to understand this property as it can have implications for the other security notions.
• Soundness: Can a cheating prover falsely convince the verifier of the correctness of a statement that is not actually correct? We refer to the probability that a cheating prover can falsely convince the verifier as the soundness error.
• Knowledge soundness: When the verifier is convinced the statement is correct, does the prover actually possess ("know") a valid witness? We refer to the probability that a cheating prover falsely convinces the verifier of this knowledge as the knowledge error.
• Zero knowledge: Does the prover learn anything besides that which can be inferred from the correctness of the statement and the prover's knowledge of a valid witness?

First, we will visit the simple definition of completeness.

Perfect Completeness. An interactive argument $(\text{Setup},\mathcal{P},\mathcal{V})$ has perfect completeness if for all polynomial-time decidable relations $\mathcal{R}$ and for all non-uniform polynomial-time adversaries $\mathcal{A}$ $$Pr\left[(x,w)\notin \mathcal{R}\vee ⟨\mathcal{P}(\mathsf{pp},x,w),\mathcal{V}(\mathsf{pp},x)⟩\text{accepts}|\begin{array}{ll}& \mathsf{pp}\leftarrow \text{Setup}(1^{\lambda })\\ & (x,w)\leftarrow \mathcal{A}(\mathsf{pp})\end{array}\right]=1$$